This feature recognizes functions annotated with #[thrust::predicate] as predicates and inserts corresponding define-fun definitions—derived from their names and arguments—into the .smt2 file. The first string literal that appears in a function's body is inserted as the predicate body.

Compared with #![thrust::raw_command], Thrust can assign a predicate name automatically and later leverage that name to connect the predicate to relevant traits(for example, SomeTrait::pred -> (define-fun some_trait_pred)).

• Example

If a user writes the following:

#[thrust::predicate]
fn is_double(x: i64, doubled_x: i64) -> bool {
    "(=
        (* x 2)
        doubled_x
    )"; true
}

the appropriate definitions are inserted into the .smt2 file.

(define-fun is_double ((x Int) (doubled_x Int)) Bool (=
        (* x 2)
        doubled_x
    ))